1. Technical Field
The present invention relates to computer verification and more particularly to decomposing bounded model checking to improve efficiency and reduce complexity for computer program verification by solving the problem in a distributed system.
2. Description of the Related Art
Bounded Model Checking (BMC) is a technique used in computer program verification. Bounded Model Checking (BMC) provides complete design coverage with respect to a correctness property for a bounded depth. In spite of using richer expressive theories to obtain compact representation, and using on-the-fly circuit simplification, each BMC instance at depth k grows bigger in size and harder to solve with successive unrolling of a design.
One possible solution is to use a distributed environment to solve each BMC instance. Due to communication overhead and inherent synchronization in such an environment, there are many challenges in achieving (even close to) linear scaling. Further, due to uneven (and often unpredictable) load and unreliable worker machines, the problem becomes all the more challenging.
Several techniques for distributed BMC have been proposed previously; however, they do not address the scalability requirement adequately.
In one distributed BMC approach, each BMC instance is partitioned structurally so that each processor gets an exclusive number of consecutive BMC time frames. The distributed problem is then solved by a distributed satisfiability (SAT), managed by a central server. Though this method overcomes the memory limitation of a single processor, and employs fine grain parallelization of SAT, it incurs significant communication overhead during the exchange of lemmas and propagation of values across partitions.
In another distributed BMC approach, each BMC instance is solved independently on a separate client. The clause learned is shared between the clients. The entire process is controlled by a master. As each BMC instance is not partitioned, there is a significant slow down as the depth increases. Further, the scalability of the method is limited by the depth d of the BMC. In other words, even if the number of processors n>>d, the method can not exploit the availability of large processors. Moreover, such an approach does not address load balancing.
In a yet another distributed BMC approach, an initial partition is generated using a partial assignment for the initial state and a property being verified. Each partition is sent to a client, which solves the BMC problem for a given depth 1 to k using the partial state assignment as initial states. This assumes that each unrolled transition after initial unrolling has symmetry, and shares clauses learned on the transition. In general, such a method is not scalable, as each client is required to solve the entire BMC problem, though for a different initial state. Also, the problem of uneven load balancing is not addressed.
One can use parallel SAT-solvers to solve BMC instances. However, parallelizing SAT solvers based on Davis-Putnam-Logeman-Loveland (DPLLs) in general incurs large communication and synchronization cost. Also, it is difficult to guide such solvers efficiently using high-level information present in the input problem.